Nuprl Lemma : iseg-subtype
11,40
postcript
pdf
A
,
B
:Type,
xs
,
ys
:(
A
List). strong-subtype(
A
;
B
)
guard((iseg(
B
;
xs
;
ys
)
iseg(
A
;
xs
;
ys
)))
latex
Definitions
subtype(
S
;
T
)
,
t
T
,
guard(
T
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
iseg(
T
;
l1
;
l2
)
,
prop{i:l}
,
x
:
A
.
B
(
x
)
,
A
c
B
,
strong-subtype(
A
;
B
)
Lemmas
strong-subtype
wf
,
iseg
wf
,
append
wf
,
strong-subtype-list
,
strong-subtype-eq3
origin
A,B:Type, xs,ys:(A List). strong-subtype(A; B) 
guard((iseg(B; xs; ys) iseg(A; xs; ys))) A,B:Type, xs,ys:(A List). strong-subtype(A; B) guard((iseg(B; xs; ys) iseg(A; xs; ys))) 
T Qx:A. B(x)
x:A. B(x)
B